g:IMonoid, a:|g|. IsMonHom{<+>hgrp,g}(n.nat(n)  a) 

latex

Up	groups 1
Definitions of Statement	|g|, IMonoid, ghgrp, n  e, <+>, <,+>, nat(n)
Definitions	t  T, x:A. B(x), t.1, <,+>, |g|, IMonoid, P  Q, f o g
Lemmas	imon wf, grp car wf, nat op mon hom 1, zhgrp to nat is hom, mon nat op wf, nat wf, int hgrp to nat wf, nat add mon wf, int add grp wf2, hgrp of ocgrp wf, mon hom p comp